COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.bb "#. Programs as objects and extensional forms."
C00005 ENDMK
C⊗;
.bb "#. Programs as objects and extensional forms."

	In previous sections, we have represented recursive programs
as functions in first order logic.  Additional freedom in manipulating
programs can be gained by representing them as objects, because
predicates and functions applicable to the programs themselves can then be
defined, and general statements about programs can be instantiated to
particular programs by substituting for bound variables, and functions
that take programs as arguments or output programs as values can be discussed.

	There are many ways of treating programs as objects; our way
is based on %2extensional forms%1.
We introduce several kinds of entities:
objects standing for functions, objects standing for expressions including
objects standing for variables and constants, and state vectors (environments)
giving values to variables.  We also have functions and predicates
defined on these domains.

	In some sense this can be regarded as a formalization of the
metamathematics of the previous sections.  In recursive function theory,
it is customary to formalize metamathematics by representing expressions,
functions, etc. by Goedel numbers so that functions on these entities
can be represented by numerical functions.
The Goedel number of any interesting expression is very large
so that their utility in recursive function theory depends on the fact
that it is never necessary to write down the Goedel number of any particular
expression.  Practical mathematical theory of computation is concerned with
proving that particular programs meet their specifications, so
we need a notation for expressions as objects
that is no more cumbersome than our usual
ways of representing recursive programs.